Inference at * 
Iof proof for Lemma p-conditional wf:


  A, B:Type, f, g:(A(B + Top)). [f?g]  A(B + Top) 

latex

 by ((Unfold `p-conditional` ( 0)) 
CollapseTHEN (Auto)) 

latex

Co.

Definitions	[f?g], x.A(x), if b then t else f fi , can-apply(f;x), suptype(S; T), f(a), S  T, x:A. B(x), x:A.B(x), Void, x:AB(x), left + right, Top, t  T, Type
Lemmas	ifthenelse wf, can-apply wf, top wf